The present invention relates generally to the field of logic design, and more specifically to increasing efficiency in liveness verification.
Liveness checking refers to the verification of properties of a logic design which are used to assess whether it will “eventually” behave in a correct way. For example, if verifying an arbiter, one may wish to check the property that “every request presented to the arbiter must eventually be granted”. Any counterexample (failure trace) to such a property must be of infinite length, showing a request which never receives a grant. Such an infinite-length trace is often represented using a finite-length trace, where some suffix of that trace—denoted by the assertion of a specially-added “LOOP” signal—is highlighted starting at a particular state, and ending with the identical state (or comparable state) about to be repeated. Semantically, this represents an infinite length counterexample since the input behavior of the suffix where LOOP is asserted may be repeated as many times as desired to witness the request-without-grant starvation scenario for an arbitrarily long duration. Liveness checking is in contrast to safety checking, where instead of checking for “eventual good” behavior, one checks if a given signal may ever assert to a given value. It is often the case that safety properties are significantly easier to solve than liveness properties.